/*
 * WinderMatrix.hpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#ifndef WINDERMATRIX_HPP_
#define WINDERMATRIX_HPP_

#include "bfr/Clause.hpp"
#include "bfr/ClauseSet.hpp"

namespace bfr {

/**
 * Class representing the Winder Matrix of a Boolean function in DNF
 * representation.
 *
 * Given a <i>positive</i> Boolean function
 * \f$f : \{ x_1, \dots, x_m \} \rightarrow \{0, 1\}\f$
 * and a DNF \f$\phi\f$ consisting of the <i>prime implicants</i> of \f$f\f$
 * (so \f$\phi\f$ represents \f$f\f$) the Winder matrix of \f$f\f$ is defined
 * as the \f$n \times n\f$ matrix \f$R\f$ s. t. \f$r_{i, d}\f$ is the number
 * of prime implicants of \f$f\f$ that contain the variable \f$x_i\f$ and
 * have exactly \f$d\f$ variables.
 *
 * (Definition from <i>Boolean Functions: Theory, Algorithms, and Applications</i>
 * by Yves Crama and Peter L. Hammer)
 *
 * For example consider the DNF
 * \f[\phi \equiv \{ \{x_1, x_2\}, \{ x_1, x_3\}, \{x_1, x_4, x_5\},
 * \{x_2, x_3, x_4\}\} \f] this DNF is prime implicant.
 *
 * The Winder matrix of this DNF (or better to say the function it represents)
 * is
 *
 * @image html winder_matrix.png
 *
 * for example the first row counts all occurrences of the variable \f$x_1\f$.
 * So the 2 in this column comes from the fact that \f$x_1\f$ occurs in 2
 * clauses of size 2.
 *
 * The last two columns contain 0 everywhere because there are no clauses of
 * size 4 or 5.
 *
 * The matrix we create contains an additional column that saves the id
 * of the variable the corresponding row was created for. So we would
 * actually save the matrix
 *
 * @image html winder_matrix_complete.png
 *
 */
class WinderMatrix {

    public:
        /**
         * Constructor.
         *
         * This constructor will initialize the matrix content.
         * If <code>create</code> is <code>true</code> it will
         * also compute the entries for the given DNF.
         *
         * Sometimes you don't want to create all the entries
         * because you have to iterate over the clause by yourself
         * or something like that.
         *
         * @param dnf The DNF containing the prime implicants.
         * @param create If <code>true</code> it will compute the values
         * of the matrix.
         */
        explicit WinderMatrix(const ClauseSet *dnf, bool create=true);

        /**
         * Create the entries of the matrix.
         *
         * This method will <b>not</b> set all values to zero
         * again. So you should call this method only once.
         *
         * It is not necessary to use this method if you used the
         * constructor with <code>create = true</code> because it
         * will call this method.
         *
         * @param dnf The DNF containing the prime implicants.
         */
        void createEntries(const ClauseSet *dnf);

        /**
         * Destructor.
         *
         * Destroys the matrix content.
         */
        ~WinderMatrix();

        /**
         * Return \f$i\f$-th row of the matrix.
         *
         * Remember that the size of the row is \f$n +1 \f$
         * where \f$n\f$ is the number of variables because on
         * the last position we save the variable id.
         *
         * @param i Row id.
         *
         * @return \f$i\f$-th row of the matrix.
         */
        inline size_t* operator[] (size_t i) const;

        /**
         * Swap two rows in the matrix.
         *
         * @param row1 Id for the first row.
         * @param row2 Id for the second row.
         */
        void swapRows(size_t row1, size_t row2);

        /**
         * Return the size of the matrix.
         *
         * The size is the number of rows in the matrix.
         *
         * @return The number of rows in the matrix.
         */
        inline size_t size() const;

        /**
         * Returns the complete content of the matrix.
         *
         * @return The matrix.
         */
        inline size_t **getMatrix() const;

        /**
         * Return the index of the variable in the specified row.
         *
         * @param row The index of the row.
         *
         * @return Variable id of the variable in row <code>row</code>,
         * this is the last value in each row.
         */
        inline size_t getVarIndex(size_t row) const;

    private:
        size_t **matrix;
        const size_t _size;
};

size_t* WinderMatrix::operator [](size_t i) const {
    return matrix[i];
}

size_t WinderMatrix::size() const {
    return _size;
}

size_t** WinderMatrix::getMatrix() const {
    return matrix;
}

size_t WinderMatrix::getVarIndex(size_t row) const {
    return matrix[row][_size];
}

}

#endif  // WINDERMATRIX_HPP_
